<html>
<head><meta charset="utf-8"><title>design meeting 2020.04.21 · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html">design meeting 2020.04.21</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="194853430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853430">(Apr 21 2020 at 19:58)</a>:</h4>
<p>Hi <span class="user-group-mention" data-user-group-id="692">@WG-traits</span></p>



<a name="194853441"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853441" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853441">(Apr 21 2020 at 19:58)</a>:</h4>
<p>meeting starting soon</p>



<a name="194853448"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853448" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853448">(Apr 21 2020 at 19:58)</a>:</h4>
<p>Agenda for today, implied bounds</p>



<a name="194853483"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853483" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853483">(Apr 21 2020 at 19:58)</a>:</h4>
<p>I think I'm gonna be fairly absent today. Work is a bit busy</p>



<a name="194853602"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853602" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853602">(Apr 21 2020 at 19:59)</a>:</h4>
<p>Before we get started, feel free to leave notes on progress</p>



<a name="194853672"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853672" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853672">(Apr 21 2020 at 20:00)</a>:</h4>
<p>and let's update the <a href="https://hackmd.io/kYWsWI9IS0213x0qX_1RDw" title="https://hackmd.io/kYWsWI9IS0213x0qX_1RDw">sprint goals doc</a></p>



<a name="194853688"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853688" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853688">(Apr 21 2020 at 20:00)</a>:</h4>
<p>There was so much activity this week</p>



<a name="194853720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853720">(Apr 21 2020 at 20:00)</a>:</h4>
<p>Including recursive solver getting merged, impl Trait</p>



<a name="194853752"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853752" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853752">(Apr 21 2020 at 20:00)</a>:</h4>
<p>Also implied bounds were discussed at the last lang meeting, can you link the doc <span class="user-mention" data-user-id="116009">@nikomatsakis</span> ?</p>



<a name="194853756"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853756" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853756">(Apr 21 2020 at 20:00)</a>:</h4>
<p>/me goes to look up what else</p>



<a name="194853769"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853769" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853769">(Apr 21 2020 at 20:01)</a>:</h4>
<p>And some work on the chalk book</p>



<a name="194853792"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853792" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853792">(Apr 21 2020 at 20:01)</a>:</h4>
<p>And also Copy, Clone and Drop support</p>



<a name="194853815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853815">(Apr 21 2020 at 20:01)</a>:</h4>
<p>I just merged the scalar types work</p>



<a name="194853821"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853821" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853821">(Apr 21 2020 at 20:01)</a>:</h4>
<p>(8 PRs merged)</p>



<a name="194853853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853853">(Apr 21 2020 at 20:01)</a>:</h4>
<p>wait, more</p>



<a name="194853960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194853960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194853960">(Apr 21 2020 at 20:02)</a>:</h4>
<p>12</p>



<a name="194854027"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854027" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854027">(Apr 21 2020 at 20:02)</a>:</h4>
<h1>Implied bounds links</h1>
<ul>
<li><a href="https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md" title="https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md">RFC 2089</a></li>
<li><a href="https://rustc-dev-guide.rust-lang.org/traits/implied-bounds.html" title="https://rustc-dev-guide.rust-lang.org/traits/implied-bounds.html">Chapter from the rustc-dev-guide</a></li>
</ul>



<a name="194854072"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854072" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854072">(Apr 21 2020 at 20:03)</a>:</h4>
<p>I was hoping to have re-read both of those but of course I didn't get to it ;)</p>



<a name="194854083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854083">(Apr 21 2020 at 20:03)</a>:</h4>
<p>but I figured we can talk out the design</p>



<a name="194854087"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854087" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854087">(Apr 21 2020 at 20:03)</a>:</h4>
<p>and I'll remember as I go</p>



<a name="194854105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854105">(Apr 21 2020 at 20:03)</a>:</h4>
<p>I'm hoping both to spread the knowledge a bit and then debate a few details</p>



<a name="194854122"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854122" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854122">(Apr 21 2020 at 20:03)</a>:</h4>
<p>let me make a dedicated hackmd for taking notes and examples I think</p>



<a name="194854169"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854169" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854169">(Apr 21 2020 at 20:03)</a>:</h4>
<p>not sure if <span class="user-mention" data-user-id="131694">@scalexm</span> is around, that'd be amazing (they're the original architect here)</p>



<a name="194854268"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854268" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854268">(Apr 21 2020 at 20:04)</a>:</h4>
<p>Oh right, this is also about the Implemented/FromEnv split, which I find confusing</p>



<a name="194854271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854271">(Apr 21 2020 at 20:04)</a>:</h4>
<p><a href="https://hackmd.io/C16wkTwoRx-aFW5F4-4CKQ" title="https://hackmd.io/C16wkTwoRx-aFW5F4-4CKQ">hackmd for notes from this meeting</a></p>



<a name="194854385"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854385" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854385">(Apr 21 2020 at 20:05)</a>:</h4>
<p>Maybe it would be helpful to start out with a brief overview of what implied bounds <em>is</em></p>



<a name="194854401"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854401" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854401">(Apr 21 2020 at 20:05)</a>:</h4>
<p>yep</p>



<a name="194854405"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854405" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854405">(Apr 21 2020 at 20:05)</a>:</h4>
<p>let me write out a proposed agenda</p>



<a name="194854406"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854406" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854406">(Apr 21 2020 at 20:05)</a>:</h4>
<p>how chalk handles it, and how it differs from rustc</p>



<a name="194854545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854545">(Apr 21 2020 at 20:06)</a>:</h4>
<h2>Agenda</h2>
<ul>
<li>What is implied bounds, from a user's POV?</li>
<li>
<p>Naive implementation and why it doesn't work<br>
    * Some of the relevant bugs and corner cases, if we can find a good list :)</p>
</li>
<li>
<p>Implementation we wound up with</p>
</li>
<li>Questions below</li>
</ul>



<a name="194854548"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854548" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854548">(Apr 21 2020 at 20:06)</a>:</h4>
<p>from the doc</p>



<a name="194854559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854559">(Apr 21 2020 at 20:06)</a>:</h4>
<p>sound reasonable?</p>



<a name="194854591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854591">(Apr 21 2020 at 20:06)</a>:</h4>
<p>(btw, did folks update the sprint goals doc?)</p>



<a name="194854596"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854596" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854596">(Apr 21 2020 at 20:06)</a>:</h4>
<p>(I'm hoping yes)</p>



<a name="194854598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854598">(Apr 21 2020 at 20:06)</a>:</h4>
<p>but let's get started</p>



<a name="194854611"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854611" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854611">(Apr 21 2020 at 20:07)</a>:</h4>
<p>if not, it'd be great to add a few notes on what you did :)</p>



<a name="194854642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854642">(Apr 21 2020 at 20:07)</a>:</h4>
<p>So, yes, implied bounds.</p>



<a name="194854646"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854646" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854646">(Apr 21 2020 at 20:07)</a>:</h4>
<p>Both rustc and chalk have a notion of "implied bounds"</p>



<a name="194854651"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854651" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854651">(Apr 21 2020 at 20:07)</a>:</h4>
<p>but rustc's is much more limited</p>



<a name="194854670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854670">(Apr 21 2020 at 20:07)</a>:</h4>
<p>as a super simple example, consider <code>trait Copy: Clone</code></p>



<a name="194854683"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854683" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854683">(Apr 21 2020 at 20:07)</a>:</h4>
<p>which expands to <code>trait Copy where Self: Clone</code></p>



<a name="194854746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854746">(Apr 21 2020 at 20:08)</a>:</h4>
<p>i.e., for every impl of <code>Copy</code>, the <code>Self</code> type must also implement <code>Clone</code></p>



<a name="194854759"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854759" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854759">(Apr 21 2020 at 20:08)</a>:</h4>
<p>more "casually" called a supertrait</p>



<a name="194854773"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854773" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854773">(Apr 21 2020 at 20:08)</a>:</h4>
<p>(supertrait does have some special meaning for <code>dyn</code> values, but let's ignore that)</p>



<a name="194854809"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854809" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854809">(Apr 21 2020 at 20:08)</a>:</h4>
<p>I can write something like</p>
<div class="codehilite"><pre><span></span><span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nb">Copy</span><span class="o">&gt;</span><span class="p">(</span><span class="n">t</span>: <span class="nc">T</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">..</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>


<p>and, because of that supertrait relationship, I can assume that <code>T: Clone</code> too</p>



<a name="194854871"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854871" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854871">(Apr 21 2020 at 20:09)</a>:</h4>
<p>But how do I know that, really? The caller only <em>directly proved</em> that <code>T: Copy</code> (well, you could imagine different designs, but let's assume that's true for the moment)</p>



<a name="194854938"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194854938" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194854938">(Apr 21 2020 at 20:09)</a>:</h4>
<p>the idea is that:</p>
<ul>
<li>the caller proved that <code>T: Copy</code> has some valid impl</li>
<li>and we know that for each valid impl of <code>T: Copy</code>, the impl proved that <code>T: Clone</code></li>
</ul>



<a name="194855035"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855035" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855035">(Apr 21 2020 at 20:10)</a>:</h4>
<p>but in Rust today if you have other where-clauses that aren't related to <code>Self</code>, you don't get these benefits</p>



<a name="194855051"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855051" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855051">(Apr 21 2020 at 20:10)</a>:</h4>
<p>e.g., <code>trait Foo&lt;X: Ord&gt;</code></p>



<a name="194855063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855063">(Apr 21 2020 at 20:10)</a>:</h4>
<p>(hi, I'm around)</p>



<a name="194855083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855083">(Apr 21 2020 at 20:10)</a>:</h4>
<p>if I have <code>fn foo&lt;A, B: Foo&lt;A&gt;&gt;()</code>, I don't get to assume that <code>A: Ord</code> (in fact, I get an error)</p>



<a name="194855127"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855127" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855127">(Apr 21 2020 at 20:11)</a>:</h4>
<p>rustc also leverages the idea of implied bounds very explicitly around lifetimes</p>



<a name="194855138"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855138" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855138">(Apr 21 2020 at 20:11)</a>:</h4>
<p>for example, if I have</p>



<a name="194855149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855149">(Apr 21 2020 at 20:11)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="k">impl</span><span class="o">&lt;</span><span class="na">&#39;a</span><span class="p">,</span><span class="w"> </span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="o">&amp;</span><span class="na">&#39;a</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">...</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="194855171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855171">(Apr 21 2020 at 20:11)</a>:</h4>
<p>the code inside the impl gets to assume that <code>T: 'a</code>, which is part of the "well-formed" conditions for the type <code>&amp;'a T</code></p>



<a name="194855250"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855250" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855250">(Apr 21 2020 at 20:12)</a>:</h4>
<p>the idea here is that the impl gets to assume all of its <em>input types</em> (<code>&amp;'a T</code>, in this case)  are "well-formed"</p>



<a name="194855263"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855263" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855263">(Apr 21 2020 at 20:12)</a>:</h4>
<p>does this all make sense so far?</p>



<a name="194855311"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855311" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855311">(Apr 21 2020 at 20:12)</a>:</h4>
<p>(in turn, whoever "applies" the impl must prove that the types are well-formed)</p>



<a name="194855357"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855357" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855357">(Apr 21 2020 at 20:12)</a>:</h4>
<p><code>T: 'a</code> meaning that <code>'a</code> lives at least as long as <code>T</code>, right?</p>



<a name="194855367"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855367" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855367">(Apr 21 2020 at 20:13)</a>:</h4>
<p>yeah</p>



<a name="194855388"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855388" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855388">(Apr 21 2020 at 20:13)</a>:</h4>
<p>more precisely, all lifetimes inside of <code>T</code> outlive <code>'a</code></p>



<a name="194855433"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855433" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855433">(Apr 21 2020 at 20:13)</a>:</h4>
<p>but we don't really have to talk about lifetimes for today, no real difference for our purposes with that example vs supertraits</p>



<a name="194855457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855457">(Apr 21 2020 at 20:13)</a>:</h4>
<p>(though there are some differences in terms of how rustc implements things which I'd prefer to avoid discussing ;)</p>



<a name="194855540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855540">(Apr 21 2020 at 20:14)</a>:</h4>
<p>Right. So, the naive implementation?</p>



<a name="194855542"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855542" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855542">(Apr 21 2020 at 20:14)</a>:</h4>
<p>so, the "user's experience" of implied bounds is to extend from "just supertraits" to a much broader set of "well-formedness" rules</p>



<a name="194855585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855585">(Apr 21 2020 at 20:14)</a>:</h4>
<p>i.e., if you have <code>trait Foo&lt;T: Ord&gt;</code>, you get to assume that <code>T: Ord</code> is true too</p>



<a name="194855593"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855593" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855593">(Apr 21 2020 at 20:14)</a>:</h4>
<p>not just supertraits</p>



<a name="194855615"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855615" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855615">(Apr 21 2020 at 20:15)</a>:</h4>
<p>similarly, and perhaps the more common example</p>



<a name="194855629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855629">(Apr 21 2020 at 20:15)</a>:</h4>
<p>if I have <code>struct MySet&lt;T: Ord&gt;</code></p>



<a name="194855645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855645">(Apr 21 2020 at 20:15)</a>:</h4>
<p>and I have an impl like:</p>
<div class="codehilite"><pre><span></span><span class="k">impl</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="n">MySet</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">...</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="194855665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855665">(Apr 21 2020 at 20:15)</a>:</h4>
<p>because I know that <code>MySet&lt;T&gt;</code> is well-formed, I would know that <code>T: Ord</code></p>



<a name="194855690"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855690" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855690">(Apr 21 2020 at 20:15)</a>:</h4>
<p>(there are some semver implications I would also prefer to avoid because it's orthogonal from our concern atm)</p>



<a name="194855780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855780">(Apr 21 2020 at 20:16)</a>:</h4>
<p>similarly <code>fn foo&lt;T&gt;(m: MySet&lt;T&gt;)</code> would know that <code>T: Ord</code> because fn parameter types must also be proven to be well-formed by callers</p>



<a name="194855857"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855857" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855857">(Apr 21 2020 at 20:17)</a>:</h4>
<p>but in terms of how we <em>implemented</em> this in chalk, we wanted to do a "simpler" impl that exposed this idea cleanly -- i.e., we wanted to capture this in the "lowering rules" that chalk-solve uses, versus something added into the solver itself or in the rust layer</p>



<a name="194855915"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855915" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855915">(Apr 21 2020 at 20:17)</a>:</h4>
<p>this is somewhat in contrast to how rustc implements supertraits, which is by a kind of "fixed point expansion". i.e., it takes an environment like <code>[T: Copy]</code> and "elaborates" it to include <code>[T: Copy, T: Clone]</code></p>



<a name="194855931"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855931" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855931">(Apr 21 2020 at 20:17)</a>:</h4>
<p>(so far so good?)</p>



<a name="194855977"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194855977" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194855977">(Apr 21 2020 at 20:18)</a>:</h4>
<p>(I'll cover the elaboration vs what chalk does in a sec)</p>



<a name="194856052"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856052" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856052">(Apr 21 2020 at 20:19)</a>:</h4>
<p>ps <span class="user-mention" data-user-id="131694">@scalexm</span> if you have a list of the various soundness bugs and edge cases, it'd be awesome if you started adding some links to <a href="https://hackmd.io/C16wkTwoRx-aFW5F4-4CKQ" title="https://hackmd.io/C16wkTwoRx-aFW5F4-4CKQ">the hackmd</a></p>



<a name="194856072"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856072" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856072">(Apr 21 2020 at 20:19)</a>:</h4>
<p>I can try to find some yes</p>



<a name="194856076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856076">(Apr 21 2020 at 20:19)</a>:</h4>
<p>well I guess in my agenda I said I would start with the "naive impl"</p>



<a name="194856097"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856097" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856097">(Apr 21 2020 at 20:19)</a>:</h4>
<p>so maybe I'll do that, though I wonder if it'd be more confusing  than helpful</p>



<a name="194856123"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856123" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856123">(Apr 21 2020 at 20:19)</a>:</h4>
<p>I guess the first idea was that we might add a rule like this</p>



<a name="194856144"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856144" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856144">(Apr 21 2020 at 20:19)</a>:</h4>
<p>given <code>trait Copy: Clone</code></p>



<a name="194856161"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856161" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856161">(Apr 21 2020 at 20:20)</a>:</h4>
<p>we might generate a clause like</p>
<div class="codehilite"><pre><span></span>Implemented(T: Clone) :- Implemented(T: Copy)
</pre></div>



<a name="194856222"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856222" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856222">(Apr 21 2020 at 20:20)</a>:</h4>
<p>in other words, if you can prove that <code>T: Copy</code>, you have proven that <code>T: Clone</code> too</p>



<a name="194856280"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856280" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856280">(Apr 21 2020 at 20:20)</a>:</h4>
<p>but this is not a very good rule</p>



<a name="194856304"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856304" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856304">(Apr 21 2020 at 20:21)</a>:</h4>
<p>ah I see <span class="user-mention" data-user-id="131694">@scalexm</span> already wrote this up perfectly in rustc-dev-guide <span aria-label="heart" class="emoji emoji-2764" role="img" title="heart">:heart:</span></p>



<a name="194856311"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856311" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856311">(Apr 21 2020 at 20:21)</a>:</h4>
<p>here is the problem</p>



<a name="194856330"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856330" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856330">(Apr 21 2020 at 20:21)</a>:</h4>
<p>now imagine I have this program</p>
<div class="codehilite"><pre><span></span><span class="k">struct</span> <span class="nc">X</span><span class="p">;</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="nb">Copy</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="194856342"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856342" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856342">(Apr 21 2020 at 20:21)</a>:</h4>
<p>this should be an error, because I don't have an <code>impl Clone for X</code></p>



<a name="194856345"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856345" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856345">(Apr 21 2020 at 20:21)</a>:</h4>
<p>but how do we find that error?</p>



<a name="194856364"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856364" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856364">(Apr 21 2020 at 20:21)</a>:</h4>
<p>the idea was that the impl would try to prove that the "where clauses" for the trait holds</p>



<a name="194856379"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856379" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856379">(Apr 21 2020 at 20:22)</a>:</h4>
<p>so the <code>impl Copy for X</code> would come with a "well-formed obligation" to prove that <code>X: Clone</code></p>



<a name="194856432"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856432" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856432">(Apr 21 2020 at 20:22)</a>:</h4>
<p>but it would also generate a program clause <code>Implemented(X: Copy)</code> (that's the rule for an impl)</p>



<a name="194856474"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856474" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856474">(Apr 21 2020 at 20:22)</a>:</h4>
<p>so if you put the clauses together, we have</p>
<div class="codehilite"><pre><span></span>Implemented(X: Copy). // from the impl

Implemented(X: Clone) :- Implemented(X: Copy). // from the trait
</pre></div>



<a name="194856491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856491">(Apr 21 2020 at 20:22)</a>:</h4>
<p>which means that, actually, the impl can prove that <code>X: Clone</code></p>



<a name="194856500"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856500" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856500">(Apr 21 2020 at 20:22)</a>:</h4>
<p>even though there is, in fact, no <code>X: Clone</code> impl anywhere</p>



<a name="194856512"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856512" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856512">(Apr 21 2020 at 20:22)</a>:</h4>
<p>basically it can prove it by relying on <em>itself</em> recursively</p>



<a name="194856539"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856539" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856539">(Apr 21 2020 at 20:23)</a>:</h4>
<p>we experimented with a few ways to address this, but we ultimately landed on the <code>FromEnv</code>/<code>Implemented</code> split you seen today</p>



<a name="194856554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856554">(Apr 21 2020 at 20:23)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21/near/194856491" title="#narrow/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21/near/194856491">said</a>:</p>
<blockquote>
<p>which means that, actually, the impl can prove that <code>X: Clone</code></p>
</blockquote>
<p>do folks see why this is?</p>



<a name="194856676"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856676" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856676">(Apr 21 2020 at 20:24)</a>:</h4>
<p>Well</p>



<a name="194856679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856679">(Apr 21 2020 at 20:24)</a>:</h4>
<p>so, the idea of <code>FromEnv</code> / <code>Implemented</code> is to kind of make this "split" apparent --</p>



<a name="194856687"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856687" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856687">(Apr 21 2020 at 20:24)</a>:</h4>
<p>/me waits</p>



<a name="194856689"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856689" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856689">(Apr 21 2020 at 20:24)</a>:</h4>
<p>That makes sense</p>



<a name="194856700"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856700" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856700">(Apr 21 2020 at 20:24)</a>:</h4>
<p>I never thought about that</p>



<a name="194856764"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856764" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856764">(Apr 21 2020 at 20:25)</a>:</h4>
<p>(sorry, I should have just thumbs up)</p>



<a name="194856796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856796">(Apr 21 2020 at 20:25)</a>:</h4>
<p>so <code>FromEnv</code> basically means "I know this is true because my caller 'proved' it for me" --</p>



<a name="194856840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856840">(Apr 21 2020 at 20:26)</a>:</h4>
<p>presuming there is a caller --</p>



<a name="194856841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mark Drobnak <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856841">(Apr 21 2020 at 20:26)</a>:</h4>
<p>Why not something like <code>Implemented(X: Copy) :- HasImpl(X: Copy), Implemented(X: Clone).</code>? (<code>HasImpl</code> would represent the impl existing in the code)</p>



<a name="194856899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856899">(Apr 21 2020 at 20:26)</a>:</h4>
<p>well, we have something that has a shape much like that iirc...</p>



<a name="194856928"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856928" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856928">(Apr 21 2020 at 20:26)</a>:</h4>
<p>though I guess its role is a bit different, but I think the <code>WellFormed</code> rule I'll discuss later at least looks like that...</p>



<a name="194856998"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194856998" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194856998">(Apr 21 2020 at 20:27)</a>:</h4>
<p>tbh I don't remember the exact reasons for this design, but there were a number of tricky cases that led us here -- it'd be good to note down some of the alternates for later perhaps -- though maybe <span class="user-mention" data-user-id="131694">@scalexm</span> remembers</p>



<a name="194857012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857012">(Apr 21 2020 at 20:27)</a>:</h4>
<p>(let's jot the question for now in the hackmd)</p>



<a name="194857105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857105">(Apr 21 2020 at 20:28)</a>:</h4>
<p>all that said, there are multiple ways to approach the problem that could be valid, and in some cases one might be more or less efficient, as well (i.e., require proving more things)</p>



<a name="194857187"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857187" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857187">(Apr 21 2020 at 20:29)</a>:</h4>
<p>for me one of the key examples to understand why we needed the split is this soundness bug: <a href="https://github.com/rust-lang/rust/pull/43786" title="https://github.com/rust-lang/rust/pull/43786">https://github.com/rust-lang/rust/pull/43786</a> (which I've put in the hackmd)</p>



<a name="194857226"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857226" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857226">(Apr 21 2020 at 20:29)</a>:</h4>
<p>I think that's one of the issue numbers I was hoping to find, yeah</p>



<a name="194857240"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857240" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857240">(Apr 21 2020 at 20:29)</a>:</h4>
<p>well, at least of all the designs we tried, the Implemented / FromEnv setup is the only one who went through this bug successfully (or other variations of it)</p>



<a name="194857367"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857367" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857367">(Apr 21 2020 at 20:30)</a>:</h4>
<p>(side note that there's a connection to the idea of coinduction and "productive definitions" here that I've never been able to quite elaborate to my satisfaction, if those terms mean anything to you)</p>



<a name="194857403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857403">(Apr 21 2020 at 20:30)</a>:</h4>
<p>but yes I remember that many "seemingly logical" designs wind up failing on that bug</p>



<a name="194857457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857457">(Apr 21 2020 at 20:31)</a>:</h4>
<p>ok, so, let's cover the scheme as impl'd today I guess</p>



<a name="194857464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857464">(Apr 21 2020 at 20:31)</a>:</h4>
<p>so the way we model this is...</p>



<a name="194857466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857466">(Apr 21 2020 at 20:31)</a>:</h4>
<p>if you have</p>



<a name="194857481"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857481" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857481">(Apr 21 2020 at 20:31)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nb">Copy</span><span class="o">&gt;</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">...</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="194857611"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857611" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857611">(Apr 21 2020 at 20:32)</a>:</h4>
<p>the <code>T: Copy</code>, in chalk terms, is a "where-clause", and it can be converted into a goal in two ways...</p>
<ul>
<li><code>Implemented(T: Copy)</code> -- "we know that <code>T: Copy</code> has an implementation"</li>
<li><code>FromEnv(T: Copy)</code> -- "we know that <code>T: Copy</code> is true because our caller proved it for us"</li>
</ul>



<a name="194857647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857647">(Apr 21 2020 at 20:32)</a>:</h4>
<p>so when you <em>call</em> <code>foo::&lt;X&gt;</code> or whatever, you have to prove <code>Implemented(X: Copy)</code></p>



<a name="194857692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857692">(Apr 21 2020 at 20:33)</a>:</h4>
<p>but when we type-check the body  of <code>foo</code>, we get to do so in an environment like </p>
<div class="codehilite"><pre><span></span>forall&lt;T&gt; {
  if (FromEnv(T: Copy)) { ... }
}
</pre></div>



<a name="194857785"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857785" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857785">(Apr 21 2020 at 20:34)</a>:</h4>
<p>similarly, when you have an <code>impl Copy for SomeType</code> impl, it generates the rule <code>Implemented(SomeType: Copy)</code> -- i.e., it lets us prove that <code>SomeType: Copy</code>, but not that we know it because of a where-clause</p>



<a name="194857824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857824">(Apr 21 2020 at 20:34)</a>:</h4>
<p>and then we have two rules. The first is:</p>



<a name="194857870"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857870" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857870">(Apr 21 2020 at 20:34)</a>:</h4>
<ul>
<li><code>forall&lt;T&gt; { Implemented(T: Copy) :- FromEnv(T: Copy) }</code></li>
</ul>



<a name="194857884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857884">(Apr 21 2020 at 20:34)</a>:</h4>
<p>(that is generated from the trait definition)</p>



<a name="194857901"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857901" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857901">(Apr 21 2020 at 20:35)</a>:</h4>
<p>if you just have that alone, you get no implied bounds, but the setup kind of "works"</p>



<a name="194857959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194857959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194857959">(Apr 21 2020 at 20:35)</a>:</h4>
<p>i.e., <code>fn foo&lt;T: Copy&gt;</code> can prove that <code>Implemented(T: Copy)</code> because:</p>
<ul>
<li>it knows <code>FromEnv(T: Copy)</code></li>
<li>and it can deduce from that <code>Implemented(T: Copy)</code> by applying the rule</li>
</ul>



<a name="194858055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858055">(Apr 21 2020 at 20:36)</a>:</h4>
<p>then the last bit is that, also from the trait definition, we generate "elaboration" rules for <code>FromEnv</code> clauses:</p>
<ul>
<li><code>forall&lt;T&gt; { FromEnv(T: Clone) :- FromEnv(T: Copy) }</code></li>
</ul>



<a name="194858079"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858079" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858079">(Apr 21 2020 at 20:36)</a>:</h4>
<p>so, <em>if you know <code>T: Copy</code> from a where-clause</em>, you also know <code>T: Clone</code> from a where-clause</p>



<a name="194858115"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858115" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858115">(Apr 21 2020 at 20:36)</a>:</h4>
<p>but if you don't have a where-clause, just a <code>Copy</code> impl, that's all you know -- that <code>T: Copy</code>, you'd have to go find the <code>T: Clone</code> impl yourself</p>



<a name="194858169"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858169" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858169">(Apr 21 2020 at 20:37)</a>:</h4>
<p>and in particular, this means that in my erroneous program above, </p>
<div class="codehilite"><pre><span></span><span class="k">struct</span> <span class="nc">X</span><span class="p">;</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="nb">Copy</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>


<p>when the impl tries to prove that <code>X: Clone</code>, it can't, because it has no where-clause to rely on.</p>



<a name="194858172"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858172" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858172">(Apr 21 2020 at 20:37)</a>:</h4>
<p>/me stops</p>



<a name="194858185"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858185" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858185">(Apr 21 2020 at 20:37)</a>:</h4>
<p>so far so good</p>



<a name="194858313"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858313" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858313">(Apr 21 2020 at 20:38)</a>:</h4>
<p>ok, let's leave aside the tricky bugs, because I want to get to some of the questions :)</p>



<a name="194858332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858332">(Apr 21 2020 at 20:39)</a>:</h4>
<p>in particular,</p>



<a name="194858344"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858344" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858344">(Apr 21 2020 at 20:39)</a>:</h4>
<p>ah well</p>



<a name="194858348"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858348" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858348">(Apr 21 2020 at 20:39)</a>:</h4>
<p>ok I left out one part :)</p>



<a name="194858362"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858362" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858362">(Apr 21 2020 at 20:39)</a>:</h4>
<p>which is to talk a bit more about what each impl must prove, and the various <code>WellFormed</code> goals</p>



<a name="194858371"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858371" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858371">(Apr 21 2020 at 20:39)</a>:</h4>
<p>and that's kind of important</p>



<a name="194858414"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858414" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858414">(Apr 21 2020 at 20:39)</a>:</h4>
<p>ps <span class="user-mention" data-user-id="131694">@scalexm</span> I hope you don't mind me typing it out, kind of useful to be sure I remember it :)</p>



<a name="194858478"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858478" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858478">(Apr 21 2020 at 20:40)</a>:</h4>
<p>right, so, I kind of hand-waived a bit about what the impl must prove</p>



<a name="194858563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858563">(Apr 21 2020 at 20:41)</a>:</h4>
<p>the idea of the "well-formed" goals is that they encapsulate two notions:</p>
<ul>
<li><code>WellFormed(Ty)</code> -- what it takes for a <em>type</em> to be well-formed (defined basd on the type definition, as we'll see)</li>
<li><code>WellFormed(T0: Trait&lt;T1..Tn&gt;)</code> -- what it takes for a <em>trait ref</em> to be well-formed (defined based on the trait definition)</li>
</ul>



<a name="194858586"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858586" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858586">(Apr 21 2020 at 20:41)</a>:</h4>
<p>(also, as I recall, we were debating about renaming at least one of those...the latter one...)</p>



<a name="194858705"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858705" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858705">(Apr 21 2020 at 20:42)</a>:</h4>
<p>so if you have <code>trait Copy: Clone</code>, it would generate a rule like this:</p>



<a name="194858718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858718">(Apr 21 2020 at 20:42)</a>:</h4>
<p>(sorry, skimming the rustc-dev-guide again :)</p>



<a name="194858790"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858790" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858790">(Apr 21 2020 at 20:43)</a>:</h4>
<div class="codehilite"><pre><span></span>forall&lt;Self&gt; {
  WellFormed(Self: Copy) :-
    Implemented(Self: Clone),
    WellFormed(Self: Clone)
}
</pre></div>


<p>(EDIT: wrong, see below)</p>



<a name="194858880"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858880" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858880">(Apr 21 2020 at 20:44)</a>:</h4>
<p>the idea is that not only must all the where-clauses on the trait be satisfied, but the <em>transitive set</em> of where-clauses from those traits too</p>



<a name="194858957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858957">(Apr 21 2020 at 20:44)</a>:</h4>
<p>time check, 45 minutes in</p>



<a name="194858961"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858961" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858961">(Apr 21 2020 at 20:44)</a>:</h4>
<p>so if you had</p>
<div class="codehilite"><pre><span></span>trait A
trait B: A
trait C: B
</pre></div>


<p>then an impl of <code>C</code> would have to prove</p>
<ul>
<li>there is an impl of <code>B</code></li>
<li>and that impl is well-formed (which implies proving that there's an impl of <code>A</code>)</li>
</ul>



<a name="194858972"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194858972" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194858972">(Apr 21 2020 at 20:44)</a>:</h4>
<p>Hmm, so <code>WellFormed(Self: Clone)</code> doesn't imply <code>Implemented(Self: Clone)</code></p>



<a name="194859035"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859035" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859035">(Apr 21 2020 at 20:45)</a>:</h4>
<p><del>remember that these are used as <em>goals</em> (things that must be proven)</del></p>



<a name="194859045"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859045" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859045">(Apr 21 2020 at 20:45)</a>:</h4>
<p>Because of coinductive semantics I think?</p>



<a name="194859172"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859172" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859172">(Apr 21 2020 at 20:46)</a>:</h4>
<p>sorry, I think I misunderstood what you were saying</p>



<a name="194859197"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859197" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859197">(Apr 21 2020 at 20:46)</a>:</h4>
<p>I think I transcribed it wrong actually</p>



<a name="194859232"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859232" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859232">(Apr 21 2020 at 20:47)</a>:</h4>
<div class="codehilite"><pre><span></span>forall&lt;Self&gt; {
  WellFormed(Self: Copy) :-
    Implemented(Self: Copy),
    WellFormed(Self: Clone)
}
</pre></div>


<p>is correct</p>



<a name="194859257"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859257" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859257">(Apr 21 2020 at 20:47)</a>:</h4>
<p>Ah, that makes more sense</p>



<a name="194859287"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859287" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859287">(Apr 21 2020 at 20:47)</a>:</h4>
<p>this is why we were debating about other names</p>



<a name="194859294"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859294" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859294">(Apr 21 2020 at 20:47)</a>:</h4>
<p>in some sense <code>WellFormed</code> is like "fully implemented"</p>



<a name="194859313"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859313" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859313">(Apr 21 2020 at 20:47)</a>:</h4>
<p>not only is the trait implemented, but also all of its where-clauses are true</p>



<a name="194859379"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859379" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mark Drobnak <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859379">(Apr 21 2020 at 20:48)</a>:</h4>
<p>(feel free to skip if meeting is going long) So <code>Implemented(T: Copy)</code> does not imply <code>Implemented(T: Clone)</code>?</p>



<a name="194859408"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859408" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859408">(Apr 21 2020 at 20:48)</a>:</h4>
<p>No, not directly</p>



<a name="194859434"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859434" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859434">(Apr 21 2020 at 20:48)</a>:</h4>
<p>Really <code>Implemented</code> should be something like <code>ExistsImpl</code>, I think</p>



<a name="194859446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859446">(Apr 21 2020 at 20:49)</a>:</h4>
<p>i.e., you know there's an impl -- but that's all you know in some sense</p>



<a name="194859456"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859456" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859456">(Apr 21 2020 at 20:49)</a>:</h4>
<p>you don't really know the impl is "well formed"</p>



<a name="194859472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859472">(Apr 21 2020 at 20:49)</a>:</h4>
<p>and that is exactly what an <code>impl Foo for T</code> gives you</p>



<a name="194859484"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859484" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mark Drobnak <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859484">(Apr 21 2020 at 20:49)</a>:</h4>
<p>It ties back to my <code>HasImpl</code> from before</p>



<a name="194859501"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859501" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859501">(Apr 21 2020 at 20:49)</a>:</h4>
<p>right, that's partly why I deferred</p>



<a name="194859539"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859539" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859539">(Apr 21 2020 at 20:49)</a>:</h4>
<p><code>ExistsImpl</code> sounds like it has to do with quantification, I think <code>Implemented</code> is fine</p>



<a name="194859625"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859625" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859625">(Apr 21 2020 at 20:50)</a>:</h4>
<p>well, anyway,</p>



<a name="194859640"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859640" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859640">(Apr 21 2020 at 20:50)</a>:</h4>
<p>I guess we won't get to the most complex part I wanted to get to, seeing as we're 50 minutes in, but we might as well try to round out the story</p>



<a name="194859644"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859644" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859644">(Apr 21 2020 at 20:50)</a>:</h4>
<p>and cover the well-formed types part of it</p>



<a name="194859649"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859649" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859649">(Apr 21 2020 at 20:50)</a>:</h4>
<p>which <em>just</em> gets to the question I wanted to raise :)</p>



<a name="194859678"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859678" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859678">(Apr 21 2020 at 20:50)</a>:</h4>
<p>I mentioned early on that <code>fn foo&lt;T&gt;(x: MySet&lt;T&gt;)</code> wants to assume that <code>T: Ord</code></p>



<a name="194859697"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859697" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859697">(Apr 21 2020 at 20:51)</a>:</h4>
<p>we've only really talked about traits here</p>



<a name="194859711"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859711" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859711">(Apr 21 2020 at 20:51)</a>:</h4>
<p>but the principles apply to type definitions in a similar way</p>



<a name="194859720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859720">(Apr 21 2020 at 20:51)</a>:</h4>
<p>if you have</p>



<a name="194859727"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859727" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859727">(Apr 21 2020 at 20:51)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="k">struct</span> <span class="nc">MySet</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nb">Ord</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="194859752"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859752" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859752">(Apr 21 2020 at 20:51)</a>:</h4>
<p>we can define a goal <code>WellFormed(MySet&lt;T&gt;)</code> that is true when that struct definition is valid...</p>



<a name="194859884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859884">(Apr 21 2020 at 20:52)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="n">WellFormed</span><span class="p">(</span><span class="n">MySet</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">)</span><span class="w"> </span>:<span class="o">-</span><span class="w"> </span><span class="n">Implemented</span><span class="p">(</span><span class="n">T</span>: <span class="nb">Ord</span><span class="p">)</span><span class="w"></span>
</pre></div>


<p>is what the rustc-dev-guide says -- i.e., it only checks that there's some impl</p>



<a name="194859901"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859901" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859901">(Apr 21 2020 at 20:52)</a>:</h4>
<p>(and we assume that the impl had to prove it was well-formed..)</p>



<a name="194859935"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859935" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859935">(Apr 21 2020 at 20:52)</a>:</h4>
<p>in any case, we also have a <code>FromEnv(Type)</code> form</p>



<a name="194859977"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194859977" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194859977">(Apr 21 2020 at 20:52)</a>:</h4>
<p>which is provable if "your environment requires <code>Type</code> to be well-formed"</p>



<a name="194860056"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860056" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860056">(Apr 21 2020 at 20:53)</a>:</h4>
<p>and we have some rules like</p>
<div class="codehilite"><pre><span></span>FromEnv(T: Ord) :- FromEnv(MySet&lt;T&gt;)
</pre></div>


<p>which we generate from the struct definition</p>



<a name="194860068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860068">(Apr 21 2020 at 20:53)</a>:</h4>
<p>i.e., each where cause in the struct generates one rule</p>



<a name="194860146"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860146" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860146">(Apr 21 2020 at 20:54)</a>:</h4>
<p>"if I'm in some context where <code>MySet&lt;T&gt;</code> must be well-formed, then I know that <code>T: Ord</code> is true too"</p>



<a name="194860195"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860195" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860195">(Apr 21 2020 at 20:54)</a>:</h4>
<p>Hm, would that work with indirection?</p>



<a name="194860206"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860206" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860206">(Apr 21 2020 at 20:54)</a>:</h4>
<p>so to put it all together, when you have </p>
<div class="codehilite"><pre><span></span><span class="k">impl</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="n">MySet</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"></span>
</pre></div>


<p>or </p>
<div class="codehilite"><pre><span></span><span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">m</span>: <span class="nc">MySet</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">)</span><span class="w"></span>
</pre></div>



<a name="194860222"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860222" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860222">(Apr 21 2020 at 20:54)</a>:</h4>
<p>they would be type-checked in an environment that includes <code>WellFormed(MySet&lt;T&gt;)</code>...</p>



<a name="194860264"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860264" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860264">(Apr 21 2020 at 20:55)</a>:</h4>
<p>...and hence they get to prove that <code>Implemented(T: Ord)</code>...</p>



<a name="194860294"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860294" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860294">(Apr 21 2020 at 20:55)</a>:</h4>
<p>...beacuse they know <code>FromEnv(T: Ord)</code>...</p>



<a name="194860307"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860307" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860307">(Apr 21 2020 at 20:55)</a>:</h4>
<p>...because they know <code>WellFormed(MySet&lt;T&gt;)</code></p>



<a name="194860320"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860320" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860320">(Apr 21 2020 at 20:55)</a>:</h4>
<p><span class="user-mention silent" data-user-id="125131">detrumi</span> <a href="#narrow/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21/near/194860195" title="#narrow/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21/near/194860195">said</a>:</p>
<blockquote>
<p>Hm, would that work with indirection?</p>
</blockquote>
<p>not sure I understand the question</p>



<a name="194860395"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860395" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860395">(Apr 21 2020 at 20:56)</a>:</h4>
<p>Never mind, I see how it works now</p>



<a name="194860413"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860413" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860413">(Apr 21 2020 at 20:56)</a>:</h4>
<p>5 minutes</p>



<a name="194860446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860446">(Apr 21 2020 at 20:56)</a>:</h4>
<p>OK, well, we <em>just</em> had time to cover the system, which makes sense :)</p>



<a name="194860517"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860517" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860517">(Apr 21 2020 at 20:57)</a>:</h4>
<p>the question I wanted to ask <span class="user-mention" data-user-id="131694">@scalexm</span> had to do with a detail of <a href="https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md" title="https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md">the RFC</a> etc, wherein we kind of do this "flatenning"</p>



<a name="194860526"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860526" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860526">(Apr 21 2020 at 20:57)</a>:</h4>
<p>I kind of glossed over it here</p>



<a name="194860552"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860552" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860552">(Apr 21 2020 at 20:57)</a>:</h4>
<p>but imagine that you have </p>
<div class="codehilite"><pre><span></span><span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">m</span>: <span class="nc">MySet</span><span class="o">&lt;</span><span class="n">SomeOtherType</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;&gt;</span><span class="p">)</span><span class="w"></span>
</pre></div>



<a name="194860569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860569">(Apr 21 2020 at 20:57)</a>:</h4>
<p>this implies <code>SomeOtherType&lt;T&gt;: Ord</code></p>



<a name="194860609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860609">(Apr 21 2020 at 20:58)</a>:</h4>
<p>but if <em>also</em> requires that <code>SomeOtherType&lt;T&gt;</code> is well-formed</p>



<a name="194860633"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860633" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860633">(Apr 21 2020 at 20:58)</a>:</h4>
<p>which may imply things about <code>T</code></p>



<a name="194860718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860718">(Apr 21 2020 at 20:59)</a>:</h4>
<p>That feels a little unintuitive</p>



<a name="194860725"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860725" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860725">(Apr 21 2020 at 20:59)</a>:</h4>
<p>the way the RFC was written, we kind of did this "elaborating" or "flatenning" when lowering from rust syntax. So we would say that <code>foo</code> is type-checked with both <code>FromEnv(MySet&lt;...&gt;)</code> and <code>FromEnv(SomeOtherType&lt;T&gt;)</code> in the environment</p>



<a name="194860772"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860772" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860772">(Apr 21 2020 at 20:59)</a>:</h4>
<p>instead of having just <code>FromEnv(MySet&lt;SomeOtherType&lt;T&gt;&gt;)</code> and then -- from <em>that</em> -- deducing that <code>FromEnv(SomeOtherType&lt;T&gt;)</code> is implied</p>



<a name="194860835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860835">(Apr 21 2020 at 21:00)</a>:</h4>
<p>(whoops, sorry, had some edits there)</p>



<a name="194860878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860878">(Apr 21 2020 at 21:00)</a>:</h4>
<p>I ran into some problems with this, I think, that have to do with higher-ranked things</p>



<a name="194860956"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860956" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860956">(Apr 21 2020 at 21:00)</a>:</h4>
<p>(we're at the hour if anyone has to go)</p>



<a name="194860991"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194860991" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194860991">(Apr 21 2020 at 21:01)</a>:</h4>
<p>and I wanted to discuss it -- i.e., if you had something like <code>for&lt;'a&gt; T: Foo&lt;&amp;'a u32&gt;</code>, you can't "elaborate" that to include <code>WellFormed(&amp;'a u32)</code>, because <code>'a</code> is bound</p>



<a name="194861007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861007">(Apr 21 2020 at 21:01)</a>:</h4>
<p>unfortunately I have to go too :)</p>



<a name="194861022"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861022" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861022">(Apr 21 2020 at 21:01)</a>:</h4>
<p>but maybe we can continue that in another topic / tomorrow...?</p>



<a name="194861050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861050">(Apr 21 2020 at 21:01)</a>:</h4>
<p>Yeah</p>



<a name="194861063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861063">(Apr 21 2020 at 21:01)</a>:</h4>
<p>hopefully it was useful to explain how the system works, in any case, and maybe prime us up for considering the follow-up questions, like maybe tweaking some of the names :)</p>



<a name="194861068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861068">(Apr 21 2020 at 21:01)</a>:</h4>
<p>and/or feature gating</p>



<a name="194861142"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861142" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861142">(Apr 21 2020 at 21:02)</a>:</h4>
<p>Thanks everyone for attending :)</p>



<a name="194861215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861215">(Apr 21 2020 at 21:03)</a>:</h4>
<p>one subtle bit that I'll note:</p>
<ul>
<li>in the system as designed, if you have a <code>T: Foo</code> where-clause, you have to <em>prove</em> that the impl exists</li>
<li>but the callee gets to assume the impl is well-formed</li>
</ul>
<p>We believe this is correct because the rust compiler is proving all impls well-formed, but it's a bit subtle.</p>
<p>We were discussing maybe changing so that instead of proving <code>Implemented(T: Foo)</code> all the time, you actually proved <code>WellFormed(T: Foo)</code>, which is in some sense "more than necessary", but also more obviously correct.</p>
<p>Moreover there was <em>some</em> situation where this made sense, maybe having to do with <code>dyn</code> values?</p>



<a name="194861244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861244">(Apr 21 2020 at 21:03)</a>:</h4>
<p>And I reminded that we were going to maybe extend the implied bound system to <code>dyn</code> values too, and that <em>too</em> was a bit subtle</p>



<a name="194861275"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861275" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861275">(Apr 21 2020 at 21:03)</a>:</h4>
<p>I think that what is said in the RFC is still true: if you have a rule of the form <code>FromEnv(T) :- FromEnv(MySet&lt;T&gt;)</code>, then you have infinite branches like <code>FromEnv(i32) :- FromEnv(MySet&lt;i32&gt;) :- FromEnv(MySet&lt;MySet&lt;i32&gt;&gt;) :- ...</code> in the proof tree, and a former version of the solver did not like it</p>



<a name="194861277"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861277" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861277">(Apr 21 2020 at 21:03)</a>:</h4>
<p>(<span class="user-mention" data-user-id="251766">@Areredify</span> you were asking some questions of a similar nature to that iirc)</p>



<a name="194861338"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861338" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861338">(Apr 21 2020 at 21:04)</a>:</h4>
<p>ah yeah</p>



<a name="194861343"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861343" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861343">(Apr 21 2020 at 21:04)</a>:</h4>
<p>but maybe that technical limitation does not exist anymore</p>



<a name="194861348"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861348" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861348">(Apr 21 2020 at 21:04)</a>:</h4>
<p>indeed that would be bad</p>



<a name="194861363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861363">(Apr 21 2020 at 21:04)</a>:</h4>
<p>well, the only way we would stop that runaway is by capping the size of the type I think</p>



<a name="194861397"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861397" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861397">(Apr 21 2020 at 21:04)</a>:</h4>
<p>which isn't really a good way</p>



<a name="194861402"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861402" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861402">(Apr 21 2020 at 21:04)</a>:</h4>
<p>though yes I'm remembering now</p>



<a name="194861404"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861404" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861404">(Apr 21 2020 at 21:04)</a>:</h4>
<p>yes, but that could "miss" legitimate proofs</p>



<a name="194861409"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861409" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861409">(Apr 21 2020 at 21:05)</a>:</h4>
<p>we had talked about some of the fancier work</p>



<a name="194861421"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861421" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861421">(Apr 21 2020 at 21:05)</a>:</h4>
<p>to identify patterns like that, too</p>



<a name="194861430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861430">(Apr 21 2020 at 21:05)</a>:</h4>
<p>yeah</p>



<a name="194861432"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861432" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861432">(Apr 21 2020 at 21:05)</a>:</h4>
<p>but I don't really want to go there :)</p>



<a name="194861468"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861468" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861468">(Apr 21 2020 at 21:05)</a>:</h4>
<p>also not sure I understand your higher ranked example where elaboration cannot work</p>



<a name="194861487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861487">(Apr 21 2020 at 21:05)</a>:</h4>
<p>yeah, I have to run, but I'll try to write out a more fully deatiled one</p>



<a name="194861495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861495">(Apr 21 2020 at 21:05)</a>:</h4>
<p>I'm not sure that it can't work exactly,</p>



<a name="194861497"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861497" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861497">(Apr 21 2020 at 21:05)</a>:</h4>
<p>ok cool</p>



<a name="194861516"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861516" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861516">(Apr 21 2020 at 21:06)</a>:</h4>
<p>I have to run too anyway</p>



<a name="194861518"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861518" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861518">(Apr 21 2020 at 21:06)</a>:</h4>
<p>but I know that when I was doing some refactoring on chalk</p>



<a name="194861557"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861557" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861557">(Apr 21 2020 at 21:06)</a>:</h4>
<p>that made the debruijn bounds more explicit</p>



<a name="194861576"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861576" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861576">(Apr 21 2020 at 21:06)</a>:</h4>
<p>ah I remember the fixme indeed</p>



<a name="194861585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861585">(Apr 21 2020 at 21:06)</a>:</h4>
<p>I identifed a place where we had overlooked the possibility of a binder</p>



<a name="194861587"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861587" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861587">(Apr 21 2020 at 21:06)</a>:</h4>
<p>I'd have to read it again</p>



<a name="194861616"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861616" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861616">(Apr 21 2020 at 21:06)</a>:</h4>
<p>ok, chat later, thanks all! (I know we said that already)</p>



<a name="194861619"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194861619" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194861619">(Apr 21 2020 at 21:06)</a>:</h4>
<p><span aria-label="wave" class="emoji emoji-1f44b" role="img" title="wave">:wave:</span></p>



<a name="194882619"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202020.04.21/near/194882619" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Charles Lew <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202020.2E04.2E21.html#194882619">(Apr 22 2020 at 02:24)</a>:</h4>
<p>By the way, that chapter in rustc-dev-guide <a href="https://github.com/rust-lang/rustc-dev-guide/pull/679" title="https://github.com/rust-lang/rustc-dev-guide/pull/679">will be gone soon</a>. The corresponding chapter in Chalk book is <a href="https://rust-lang.github.io/chalk/book/clauses/implied_bounds.html" title="https://rust-lang.github.io/chalk/book/clauses/implied_bounds.html">https://rust-lang.github.io/chalk/book/clauses/implied_bounds.html</a> .</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>